And then we tested the whole thing for the one post case.

Remember we had this kind of cave like one post domain.

We have some initial information which we can describe in propositional logic.

And then we can transform the description into clause normal form and then make a resolution proof.

That tells us the one post is at a certain place.

Which is good to know because if we know that we can kill the one post and then research for the gold.